* Step 1: WeightGap WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            dx(X) -> one()
            dx(a()) -> zero()
            dx(div(ALPHA,BETA)) -> minus(div(dx(ALPHA),BETA),times(ALPHA,div(dx(BETA),exp(BETA,two()))))
            dx(exp(ALPHA,BETA)) -> plus(times(BETA,times(exp(ALPHA,minus(BETA,one())),dx(ALPHA)))
                                       ,times(exp(ALPHA,BETA),times(ln(ALPHA),dx(BETA))))
            dx(ln(ALPHA)) -> div(dx(ALPHA),ALPHA)
            dx(minus(ALPHA,BETA)) -> minus(dx(ALPHA),dx(BETA))
            dx(neg(ALPHA)) -> neg(dx(ALPHA))
            dx(plus(ALPHA,BETA)) -> plus(dx(ALPHA),dx(BETA))
            dx(times(ALPHA,BETA)) -> plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA)))
        - Signature:
            {dx/1} / {a/0,div/2,exp/2,ln/1,minus/2,neg/1,one/0,plus/2,times/2,two/0,zero/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {dx} and constructors {a,div,exp,ln,minus,neg,one,plus
            ,times,two,zero}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(div) = {1},
            uargs(minus) = {1,2},
            uargs(neg) = {1},
            uargs(plus) = {1,2},
            uargs(times) = {2}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                p(a) = [0]                  
              p(div) = [1] x1 + [0]         
               p(dx) = [1]                  
              p(exp) = [1] x2 + [2]         
               p(ln) = [2]                  
            p(minus) = [1] x1 + [1] x2 + [1]
              p(neg) = [1] x1 + [0]         
              p(one) = [0]                  
             p(plus) = [1] x1 + [1] x2 + [5]
            p(times) = [1] x2 + [0]         
              p(two) = [1]                  
             p(zero) = [0]                  
          
          Following rules are strictly oriented:
            dx(X) = [1]   
                  > [0]   
                  = one() 
          
          dx(a()) = [1]   
                  > [0]   
                  = zero()
          
          
          Following rules are (at-least) weakly oriented:
            dx(div(ALPHA,BETA)) =  [1]                                                                  
                                >= [3]                                                                  
                                =  minus(div(dx(ALPHA),BETA),times(ALPHA,div(dx(BETA),exp(BETA,two()))))
          
            dx(exp(ALPHA,BETA)) =  [1]                                                                  
                                >= [7]                                                                  
                                =  plus(times(BETA,times(exp(ALPHA,minus(BETA,one())),dx(ALPHA)))       
                                       ,times(exp(ALPHA,BETA),times(ln(ALPHA),dx(BETA))))               
          
                  dx(ln(ALPHA)) =  [1]                                                                  
                                >= [1]                                                                  
                                =  div(dx(ALPHA),ALPHA)                                                 
          
          dx(minus(ALPHA,BETA)) =  [1]                                                                  
                                >= [3]                                                                  
                                =  minus(dx(ALPHA),dx(BETA))                                            
          
                 dx(neg(ALPHA)) =  [1]                                                                  
                                >= [1]                                                                  
                                =  neg(dx(ALPHA))                                                       
          
           dx(plus(ALPHA,BETA)) =  [1]                                                                  
                                >= [7]                                                                  
                                =  plus(dx(ALPHA),dx(BETA))                                             
          
          dx(times(ALPHA,BETA)) =  [1]                                                                  
                                >= [7]                                                                  
                                =  plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA)))                    
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 2: NaturalPI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            dx(div(ALPHA,BETA)) -> minus(div(dx(ALPHA),BETA),times(ALPHA,div(dx(BETA),exp(BETA,two()))))
            dx(exp(ALPHA,BETA)) -> plus(times(BETA,times(exp(ALPHA,minus(BETA,one())),dx(ALPHA)))
                                       ,times(exp(ALPHA,BETA),times(ln(ALPHA),dx(BETA))))
            dx(ln(ALPHA)) -> div(dx(ALPHA),ALPHA)
            dx(minus(ALPHA,BETA)) -> minus(dx(ALPHA),dx(BETA))
            dx(neg(ALPHA)) -> neg(dx(ALPHA))
            dx(plus(ALPHA,BETA)) -> plus(dx(ALPHA),dx(BETA))
            dx(times(ALPHA,BETA)) -> plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA)))
        - Weak TRS:
            dx(X) -> one()
            dx(a()) -> zero()
        - Signature:
            {dx/1} / {a/0,div/2,exp/2,ln/1,minus/2,neg/1,one/0,plus/2,times/2,two/0,zero/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {dx} and constructors {a,div,exp,ln,minus,neg,one,plus
            ,times,two,zero}
    + Applied Processor:
        NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a polynomial interpretation of kind constructor-based(mixed(2)):
        The following argument positions are considered usable:
          uargs(div) = {1},
          uargs(minus) = {1,2},
          uargs(neg) = {1},
          uargs(plus) = {1,2},
          uargs(times) = {2}
        
        Following symbols are considered usable:
          {dx}
        TcT has computed the following interpretation:
              p(a) = 1            
            p(div) = 1 + x1 + x2  
             p(dx) = 4*x1 + 5*x1^2
            p(exp) = 1 + x1 + x2  
             p(ln) = 1 + x1       
          p(minus) = 1 + x1 + x2  
            p(neg) = x1           
            p(one) = 0            
           p(plus) = 1 + x1 + x2  
          p(times) = 1 + x1 + x2  
            p(two) = 0            
           p(zero) = 0            
        
        Following rules are strictly oriented:
          dx(div(ALPHA,BETA)) = 9 + 14*ALPHA + 10*ALPHA*BETA + 5*ALPHA^2 + 14*BETA + 5*BETA^2        
                              > 5 + 5*ALPHA + 5*ALPHA^2 + 6*BETA + 5*BETA^2                          
                              = minus(div(dx(ALPHA),BETA),times(ALPHA,div(dx(BETA),exp(BETA,two()))))
        
                dx(ln(ALPHA)) = 9 + 14*ALPHA + 5*ALPHA^2                                             
                              > 1 + 5*ALPHA + 5*ALPHA^2                                              
                              = div(dx(ALPHA),ALPHA)                                                 
        
        dx(minus(ALPHA,BETA)) = 9 + 14*ALPHA + 10*ALPHA*BETA + 5*ALPHA^2 + 14*BETA + 5*BETA^2        
                              > 1 + 4*ALPHA + 5*ALPHA^2 + 4*BETA + 5*BETA^2                          
                              = minus(dx(ALPHA),dx(BETA))                                            
        
         dx(plus(ALPHA,BETA)) = 9 + 14*ALPHA + 10*ALPHA*BETA + 5*ALPHA^2 + 14*BETA + 5*BETA^2        
                              > 1 + 4*ALPHA + 5*ALPHA^2 + 4*BETA + 5*BETA^2                          
                              = plus(dx(ALPHA),dx(BETA))                                             
        
        dx(times(ALPHA,BETA)) = 9 + 14*ALPHA + 10*ALPHA*BETA + 5*ALPHA^2 + 14*BETA + 5*BETA^2        
                              > 3 + 5*ALPHA + 5*ALPHA^2 + 5*BETA + 5*BETA^2                          
                              = plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA)))                    
        
        
        Following rules are (at-least) weakly oriented:
                      dx(X) =  4*X + 5*X^2                                                   
                            >= 0                                                             
                            =  one()                                                         
        
                    dx(a()) =  9                                                             
                            >= 0                                                             
                            =  zero()                                                        
        
        dx(exp(ALPHA,BETA)) =  9 + 14*ALPHA + 10*ALPHA*BETA + 5*ALPHA^2 + 14*BETA + 5*BETA^2 
                            >= 9 + 7*ALPHA + 5*ALPHA^2 + 7*BETA + 5*BETA^2                   
                            =  plus(times(BETA,times(exp(ALPHA,minus(BETA,one())),dx(ALPHA)))
                                   ,times(exp(ALPHA,BETA),times(ln(ALPHA),dx(BETA))))        
        
             dx(neg(ALPHA)) =  4*ALPHA + 5*ALPHA^2                                           
                            >= 4*ALPHA + 5*ALPHA^2                                           
                            =  neg(dx(ALPHA))                                                
        
* Step 3: NaturalPI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            dx(exp(ALPHA,BETA)) -> plus(times(BETA,times(exp(ALPHA,minus(BETA,one())),dx(ALPHA)))
                                       ,times(exp(ALPHA,BETA),times(ln(ALPHA),dx(BETA))))
            dx(neg(ALPHA)) -> neg(dx(ALPHA))
        - Weak TRS:
            dx(X) -> one()
            dx(a()) -> zero()
            dx(div(ALPHA,BETA)) -> minus(div(dx(ALPHA),BETA),times(ALPHA,div(dx(BETA),exp(BETA,two()))))
            dx(ln(ALPHA)) -> div(dx(ALPHA),ALPHA)
            dx(minus(ALPHA,BETA)) -> minus(dx(ALPHA),dx(BETA))
            dx(plus(ALPHA,BETA)) -> plus(dx(ALPHA),dx(BETA))
            dx(times(ALPHA,BETA)) -> plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA)))
        - Signature:
            {dx/1} / {a/0,div/2,exp/2,ln/1,minus/2,neg/1,one/0,plus/2,times/2,two/0,zero/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {dx} and constructors {a,div,exp,ln,minus,neg,one,plus
            ,times,two,zero}
    + Applied Processor:
        NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a polynomial interpretation of kind constructor-based(mixed(2)):
        The following argument positions are considered usable:
          uargs(div) = {1},
          uargs(minus) = {1,2},
          uargs(neg) = {1},
          uargs(plus) = {1,2},
          uargs(times) = {2}
        
        Following symbols are considered usable:
          {dx}
        TcT has computed the following interpretation:
              p(a) = 1            
            p(div) = 1 + x1 + x2  
             p(dx) = 5*x1 + 4*x1^2
            p(exp) = 1 + x1 + x2  
             p(ln) = 1 + x1       
          p(minus) = 1 + x1 + x2  
            p(neg) = 1 + x1       
            p(one) = 0            
           p(plus) = x1 + x2      
          p(times) = 1 + x1 + x2  
            p(two) = 1            
           p(zero) = 0            
        
        Following rules are strictly oriented:
        dx(exp(ALPHA,BETA)) = 9 + 13*ALPHA + 8*ALPHA*BETA + 4*ALPHA^2 + 13*BETA + 4*BETA^2  
                            > 8 + 8*ALPHA + 4*ALPHA^2 + 8*BETA + 4*BETA^2                   
                            = plus(times(BETA,times(exp(ALPHA,minus(BETA,one())),dx(ALPHA)))
                                  ,times(exp(ALPHA,BETA),times(ln(ALPHA),dx(BETA))))        
        
             dx(neg(ALPHA)) = 9 + 13*ALPHA + 4*ALPHA^2                                      
                            > 1 + 5*ALPHA + 4*ALPHA^2                                       
                            = neg(dx(ALPHA))                                                
        
        
        Following rules are (at-least) weakly oriented:
                        dx(X) =  5*X + 4*X^2                                                          
                              >= 0                                                                    
                              =  one()                                                                
        
                      dx(a()) =  9                                                                    
                              >= 0                                                                    
                              =  zero()                                                               
        
          dx(div(ALPHA,BETA)) =  9 + 13*ALPHA + 8*ALPHA*BETA + 4*ALPHA^2 + 13*BETA + 4*BETA^2         
                              >= 6 + 6*ALPHA + 4*ALPHA^2 + 7*BETA + 4*BETA^2                          
                              =  minus(div(dx(ALPHA),BETA),times(ALPHA,div(dx(BETA),exp(BETA,two()))))
        
                dx(ln(ALPHA)) =  9 + 13*ALPHA + 4*ALPHA^2                                             
                              >= 1 + 6*ALPHA + 4*ALPHA^2                                              
                              =  div(dx(ALPHA),ALPHA)                                                 
        
        dx(minus(ALPHA,BETA)) =  9 + 13*ALPHA + 8*ALPHA*BETA + 4*ALPHA^2 + 13*BETA + 4*BETA^2         
                              >= 1 + 5*ALPHA + 4*ALPHA^2 + 5*BETA + 4*BETA^2                          
                              =  minus(dx(ALPHA),dx(BETA))                                            
        
         dx(plus(ALPHA,BETA)) =  5*ALPHA + 8*ALPHA*BETA + 4*ALPHA^2 + 5*BETA + 4*BETA^2               
                              >= 5*ALPHA + 4*ALPHA^2 + 5*BETA + 4*BETA^2                              
                              =  plus(dx(ALPHA),dx(BETA))                                             
        
        dx(times(ALPHA,BETA)) =  9 + 13*ALPHA + 8*ALPHA*BETA + 4*ALPHA^2 + 13*BETA + 4*BETA^2         
                              >= 2 + 6*ALPHA + 4*ALPHA^2 + 6*BETA + 4*BETA^2                          
                              =  plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA)))                    
        
* Step 4: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak TRS:
            dx(X) -> one()
            dx(a()) -> zero()
            dx(div(ALPHA,BETA)) -> minus(div(dx(ALPHA),BETA),times(ALPHA,div(dx(BETA),exp(BETA,two()))))
            dx(exp(ALPHA,BETA)) -> plus(times(BETA,times(exp(ALPHA,minus(BETA,one())),dx(ALPHA)))
                                       ,times(exp(ALPHA,BETA),times(ln(ALPHA),dx(BETA))))
            dx(ln(ALPHA)) -> div(dx(ALPHA),ALPHA)
            dx(minus(ALPHA,BETA)) -> minus(dx(ALPHA),dx(BETA))
            dx(neg(ALPHA)) -> neg(dx(ALPHA))
            dx(plus(ALPHA,BETA)) -> plus(dx(ALPHA),dx(BETA))
            dx(times(ALPHA,BETA)) -> plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA)))
        - Signature:
            {dx/1} / {a/0,div/2,exp/2,ln/1,minus/2,neg/1,one/0,plus/2,times/2,two/0,zero/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {dx} and constructors {a,div,exp,ln,minus,neg,one,plus
            ,times,two,zero}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^2))